Termination Proof Script
Consider the TRS R consisting of the rewrite rules
|
| 1: |
|
p(f(f(x))) |
→ q(f(g(x))) |
| 2: |
|
p(g(g(x))) |
→ q(g(f(x))) |
| 3: |
|
q(f(f(x))) |
→ p(f(g(x))) |
| 4: |
|
q(g(g(x))) |
→ p(g(f(x))) |
|
There are 4 dependency pairs:
|
| 5: |
|
P(f(f(x))) |
→ Q(f(g(x))) |
| 6: |
|
P(g(g(x))) |
→ Q(g(f(x))) |
| 7: |
|
Q(f(f(x))) |
→ P(f(g(x))) |
| 8: |
|
Q(g(g(x))) |
→ P(g(f(x))) |
|
The approximated dependency graph contains no SCCs
and hence the TRS is trivially terminating.
Tyrolean Termination Tool (0.01 seconds)
--- May 3, 2006